package app;

import com.alibaba.fastjson.JSONArray;
import com.alibaba.fastjson.JSONObject;
import common.struct.CheckInfo;
import common.struct.InvServiceConfig;
import common.struct.SensorData;
import common.struct.ConstantEnum.CheckResult;
import common.struct.ConstantEnum.SensorDataType;
import common.util.Util;
import org.apache.commons.logging.Log;
import org.apache.commons.logging.LogFactory;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.regex.Matcher;
import java.util.regex.Pattern;

public class InvCheck {
    private Log logger = LogFactory.getLog(InvCheck.class);
    private static InvCheck instance;
    AppRemoteConnector connector;
//    private Map<Integer, List<String>> checkMap;
//    private Map<Integer, List<String>> monitorMap;
//    private Map<Integer, List<String>> isMonitoredMap;
//    private Map<Integer, Integer> iterIdMap = new HashMap<>();
    //第一维是“文件名[行号]”作为标识，第二维是参数列表
    private Map<String, List<String>> checkMap;
    private Map<String, List<String>> monitorMap;
    private Map<String, List<String>> isMonitoredMap;
    private Map<String, List<String>> iterIdMap = new HashMap<>();
    private boolean checkFilesFlag;

    public static InvCheck getInstance() {
        if (instance == null) {
            synchronized (InvCheck.class) {
                if (instance == null) {
                    instance = new InvCheck();
                }
            }
        }
        return instance;
    }

    private InvCheck() {
        checkMap = new HashMap<>();
        monitorMap = new HashMap<>();
        isMonitoredMap = new HashMap<>();
        checkFilesFlag = false;
//        String fileName = "test/main/java/"
//                + Thread.currentThread().getStackTrace()[4].getClassName().replace(".", "/")
//                + ".java";
//        //打印fileName中的内容
//        String[] content = Util.readFileContent(fileName).split("\n");
//        for (int i = 0; i < content.length; i++) {
//            Pattern checkPattern = Pattern.compile("check\\((\\w+(,\\s*\\w+)*)\\)"); // 匹配括号中的多个单词的正则表达式
//            Matcher checkMatcher = checkPattern.matcher(content[i]);
//            if (checkMatcher.find()) {
//                String[] params = checkMatcher.group(1).split(",\\s*"); // 将匹配到的参数字符串按逗号分隔成数组
//                checkMap.put(i + 1, List.of(params));
//            }
//
//            Pattern monitorPattern = Pattern.compile("monitor\\((\\w+(,\\s*\\w+)*)\\)");
//            Matcher monitorMatcher = monitorPattern.matcher(content[i]);
//            if (monitorMatcher.find()) {
//                String[] params = monitorMatcher.group(1).split(",\\s*");
//                monitorMap.put(i + 1, List.of(params));
//            }
//
//            Pattern isMonitoredPattern = Pattern.compile("isMonitored\\((\\w+(,\\s*\\w+)*)\\)");
//            Matcher isMonitoredMatcher = isMonitoredPattern.matcher(content[i]);
//            if (isMonitoredMatcher.find()) {
//                String[] params = isMonitoredMatcher.group(1).split(",\\s*");
//                isMonitoredMap.put(i + 1, List.of(params));
//            }
//        }
//        System.out.println(checkMap);
//        System.out.println(monitorMap);
//        System.out.println(isMonitoredMap);
    }

    public void init(InvServiceConfig config) {
        if (config.getChkFiles() != null) {
            checkFilesFlag = true;
            for (String fileName : config.getChkFiles()) {
                String simpleFileName = Util.extractSimpleFileName(fileName);
                String[] content = Util.readFileContent(fileName).split("\n");
                for (int i = 0; i < content.length; i++) {
                    Pattern checkPattern = Pattern.compile("check\\((\\w+(,\\s*\\w+)*)\\)"); // 匹配括号中的多个单词的正则表达式
                    Matcher checkMatcher = checkPattern.matcher(content[i]);
                    if (checkMatcher.find()) {
                        String[] params = checkMatcher.group(1).split(",\\s*"); // 将匹配到的参数字符串按逗号分隔成数组
                        checkMap.put(simpleFileName + "[" + (i + 1) + "]", List.of(params));
                    }

                    Pattern monitorPattern = Pattern.compile("monitor\\((\\w+(,\\s*\\w+)*)\\)");
                    Matcher monitorMatcher = monitorPattern.matcher(content[i]);
                    if (monitorMatcher.find()) {
                        String[] params = monitorMatcher.group(1).split(",\\s*");
                        monitorMap.put(simpleFileName + "[" + (i + 1) + "]", List.of(params));
                    }

                    Pattern isMonitoredPattern = Pattern.compile("isMonitored\\((\\w+(,\\s*\\w+)*)\\)");
                    Matcher isMonitoredMatcher = isMonitoredPattern.matcher(content[i]);
                    if (isMonitoredMatcher.find()) {
                        String[] params = isMonitoredMatcher.group(1).split(",\\s*");
                        isMonitoredMap.put(simpleFileName + "[" + (i + 1) + "]", List.of(params));
                    }
                }
            }
        }
    }

//    public boolean bind(AppRemoteConnector connector) {
//        if (connector == null) {
//            logger.info("[InvCheck]: bind(connector) -> false");
//            return false;
//        }
//        this.connector = connector;
//        logger.info(String.format("[%s]: bind(connector) -> true", connector.getAppName()));
//        return true;
//    }

    public boolean monitor(Object... objs) {
        StackTraceElement stackTraceElement = Thread.currentThread().getStackTrace()[2];
        int lineNumber = stackTraceElement.getLineNumber();
        String fileName = Util.extractSimpleFileName(stackTraceElement.getFileName());
        String id = fileName + "[" + lineNumber + "]";
        if (connector == null) {
            logger.error(String.format("[InvCheck]: monitor[file: %s, line: %d] -> %s",
                    fileName, lineNumber, false));
            return false;
        }
        if (checkFilesFlag) {
            List<String> params = monitorMap.get(id);
            if (params == null) {
                logger.error(String.format("[InvCheck]: monitor[file: %s, line: %d] -> %s",
                        fileName, lineNumber, false));
                return false;
            }
            JSONObject jo = new JSONObject(3);
            jo.put("app_name", connector.getAppName());
            jo.put("api", "inv_monitor");
            JSONArray ja = new JSONArray();
            ja.addAll(params);
            jo.put("objs", ja);
            connector.getTCP().send(jo.toJSONString());

            boolean state = false;
            String recv = connector.getTCP().recv();
            if (recv != null) {
                JSONObject retJson = JSONObject.parseObject(recv);
                state = retJson.getBoolean("state");
            }
            logger.info(String.format("[%s]: monitor%s -> %s", connector.getAppName(), monitorMap.get(id), state));
            return state;
        } else {
            logger.warn(String.format("[InvCheck]: monitor[file: %s, line: %d] -> %s",
                    fileName, lineNumber, false));
            return false;
        }
    }

    public boolean isMonitored(Object... objs) {
        StackTraceElement stackTraceElement = Thread.currentThread().getStackTrace()[2];
        int lineNumber = stackTraceElement.getLineNumber();
        String fileName = Util.extractSimpleFileName(stackTraceElement.getFileName());
        String id = fileName + "[" + lineNumber + "]";
        if (connector == null) {
            logger.error(String.format("[InvCheck]: isMonitored[file: %s, line: %d] -> %s",
                    fileName, lineNumber, false));
            return false;
        }
        if (checkFilesFlag) {
            List<String> params = isMonitoredMap.get(id);
            if (params == null) {
                logger.error(String.format("[InvCheck]: isMonitored[file: %s, line: %d] -> %s",
                        fileName, lineNumber, false));
                return false;
            }
            JSONObject jo = new JSONObject(3);
            jo.put("app_name", connector.getAppName());
            jo.put("api", "inv_is_monitored");
            JSONArray ja = new JSONArray();
            ja.addAll(params);
            jo.put("objs", ja);
            connector.getTCP().send(jo.toJSONString());

            boolean state = false;
            String recv = connector.getTCP().recv();
            if (recv != null) {
                JSONObject retJson = JSONObject.parseObject(recv);
                state = retJson.getBoolean("state");
            }
            logger.info(String.format("[%s]: isMonitored%s -> %s", connector.getAppName(), isMonitoredMap.get(id),
                    state));
            return state;
        } else {
            logger.warn(String.format("[InvCheck]: isMonitored[file: %s, line: %d] -> %s",
                    fileName, lineNumber, false));
            return false;
        }
    }

    public boolean check(Object... objs) {
//        int lineNumber = Thread.currentThread().getStackTrace()[2].getLineNumber();
//        if (connector == null) {
//            logger.info(String.format("[InvCheck]: check%s -> %s",
//                    isMonitoredMap.get(lineNumber), false));
//            return false;
//        }
//
//        if (!iterIdMap.containsKey(lineNumber)) {
//            iterIdMap.put(lineNumber, 1);
//        }
//        int iterId = iterIdMap.get(lineNumber);
//        iterIdMap.put(lineNumber, iterId + 1);
//
//        List<String> params = checkMap.get(lineNumber);
        StackTraceElement stackTraceElement = Thread.currentThread().getStackTrace()[2];
        int lineNumber = stackTraceElement.getLineNumber();
        String fileName = Util.extractSimpleFileName(stackTraceElement.getFileName());
        String id = fileName + "[" + lineNumber + "]";
        if (connector == null) {
            logger.error(String.format("[InvCheck]: check[file: %s, line: %d] -> %s",
                    fileName, lineNumber, false));
            return false;
        }
        List<String> params = null;
        if (checkFilesFlag) {
            params = checkMap.get(id);
            if (params == null) {
                logger.error(String.format("[InvCheck]: check[file: %s, line: %d] -> %s",
                        fileName, lineNumber, false));
                return false;
            }
        } else {
            int size = objs.length;
            if (size == 0) {
                logger.error(String.format("[InvCheck]: check[file: %s, line: %d] -> %s",
                        fileName, lineNumber, false));
                return false;
            }
            params = new ArrayList<>();
            for (int i = 1; i <= size; i++) {
                params.add("arg" + i);
            }
        }
        JSONObject jo = new JSONObject(6);
        jo.put("app_name", connector.getAppName());
        jo.put("api", "inv_check");
        JSONObject joo = new JSONObject(true);
        for (int i = 0; i < params.size(); i++) {
            joo.put(params.get(i), objs[i]);
        }
        jo.put("objs", joo);
        jo.put("line_number", id); //TODO:这里的line_number是文件名[行号]
        jo.put("check_time", System.currentTimeMillis());
        jo.put("iter_id", iterIdMap.get(id));
        connector.getTCP().send(jo.toJSONString());

        boolean state = false;
        String recv = connector.getTCP().recv();
        if (recv != null) {
            JSONObject retJson = JSONObject.parseObject(recv);
            state = retJson.getBoolean("state");
        }
        logger.info(String.format("[%s]: check%s -> %s", connector.getAppName(), params,
                state));
        return state;
    }

    public boolean saveTo(String fileName) {
        if (connector == null) {
            logger.info(String.format("[InvCheck]: saveTo(%s) -> %s",
                    fileName, false));
            return false;
        }

        JSONObject jo = new JSONObject(2);
        jo.put("app_name", connector.getAppName());
        jo.put("api", "inv_save");
        connector.getTCP().send(jo.toJSONString());

        boolean state = false;
        String recv = connector.getTCP().recv();
        try {
            JSONObject retJson = JSONObject.parseObject(recv);
            String content = retJson.get("content").toString();
            int index = fileName.lastIndexOf('/');
            String dir = index == -1 ? "output" : fileName.substring(0, index);
            String name = fileName.substring(index + 1);
            Util.writeFileContent(dir, name, content);
            state = true;
        } catch (Exception e) {}
        logger.info(String.format("[%s]: saveTo(%s) -> %s", connector.getAppName(), fileName,
                state));
        return state;
    }

    public boolean loadFrom(String fileName) {
        if (connector == null) {
            logger.info(String.format("[InvCheck]: loadFrom(%s) -> %s",
                    fileName, false));
            return false;
        }

        JSONObject jo = new JSONObject(3);
        jo.put("app_name", connector.getAppName());
        jo.put("api", "inv_load");
        int index = fileName.lastIndexOf('/');
        String dir = index == -1 ? "output" : fileName.substring(0, index);
        String name = fileName.substring(index + 1);
        jo.put("content", JSONObject.parseObject(Util.readFileContent(dir + "/" + name)));
        connector.getTCP().send(jo.toJSONString());

        boolean state = false;
        String recv = connector.getTCP().recv();
        if (recv != null) {
            JSONObject retJson = JSONObject.parseObject(recv);
            state = retJson.getBoolean("state");
        }
        logger.info(String.format("[%s]: loadFrom(%s) -> %s", connector.getAppName(), fileName,
                state));
        return state;
    }

    public boolean checkGenerated() {
        if (connector == null) {
            logger.info(String.format("[InvCheck]: checkGenerated() -> %s",
                    false));
            return false;
        }

        JSONObject jo = new JSONObject(2);
        jo.put("app_name", connector.getAppName());
        jo.put("api", "inv_check_generated");
        connector.getTCP().send(jo.toJSONString());

        boolean state = false;
        String recv = connector.getTCP().recv();
        if (recv != null) {
            JSONObject retJson = JSONObject.parseObject(recv);
            state = retJson.getBoolean("state");
        }
        logger.info(String.format("[%s]: checkGenerated() -> %s", connector.getAppName(),
                state));
        return state;
    }

    //TODO:获取不变式是否每个group已生成不变式，config里面添加不分组开关

    public CheckResult getResult(SensorData data) {
        if (data.getType() != SensorDataType.INV_REPORT) {
//            logger.info(String.format("[%s]: getResult(data) -> null", connector.getAppName()));
            return null;
        }
        //        logger.info(String.format("[%s]: getResult(data) -> %s", connector.getAppName(), ret));
        return CheckResult.fromString((String) data.getData("result"));
    }

    public CheckInfo getInfo(SensorData data) {
        if (data.getType() != SensorDataType.INV_REPORT) {
//            logger.info(String.format("[%s]: getInfo(data) -> null", connector.getAppName()));
            return null;
        }
        //        logger.info(String.format("[%s]: getInfo(data) -> %s", connector.getAppName(), ret));
        String lindId = (String) data.getData("line_number");
        int lineNumber = Integer.parseInt(lindId.substring(lindId.indexOf("[") + 1, lindId.indexOf("]")));
        return new CheckInfo(
                (String) data.getData("name"),
                lineNumber,
                (Integer) data.getData("iter_id"),
                (Long) data.getData("check_time"),
                CheckResult.fromString((String) data.getData("result")));
    }
}


